Skip to content

Autoharness: Derive Arbitrary for structs and enums #4167

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 6 commits into from
Jun 27, 2025
Merged

Autoharness: Derive Arbitrary for structs and enums #4167

merged 6 commits into from
Jun 27, 2025

Conversation

@carolynzech
Copy link
Contributor

@carolynzech carolynzech commented Jun 19, 2025 •
edited
Loading

While generating automatic harnesses, derive Arbitrary implementations for structs and enums that don't have implementations.

Implementation Overview

  1. In automatic_harness_partition, we mark a function as eligible for autoharness if its arguments either:
    a. implement Arbitrary, or
    b. are structs/enums whose fields implement Arbitrary.
  2. AutomaticHarnessPass runs as before, but now may generate harnesses that call kani::any() for structs/enums that do not actually implement Arbitrary. See the definition of kani::any():

    kani/library/kani_core/src/lib.rs

    Lines 274 to 276 in b64e59d

    pub fn any<T: Arbitrary>() -> T {
    T::any()
    }

    The initial kani::any() call resolves fine, but the compiler would ICE if it tried to resolve T::any().
  3. To avoid the ICE, we add a new AutomaticArbitraryPass that runs after the AutomaticHarnessPass. This pass detects the calls to nonexistent T::any()s and replaces them with inlined T::any() implementations. These implementations are based on what Kani's derive macros for structs and enums produce.

Example

Given the automatic harness foo_harness produced by AutomaticHarnessPass:

struct Foo(u32)
fn function_with_foo(foo: Foo) { ... }

// pretend this is an autoharness, just written in source code for the example
#[kani::proof]
fn foo_harness() {
  let foo = kani::any();
  function_with_foo(foo);
}

AutomaticArbitraryPass will rewrite kani::any():

pub fn any() -> Foo {
    Foo::any()
}

as:

pub fn any() -> Foo {
  Self(kani::any())
}

i.e., replace the call to Foo::any() with what the derive macro would have produced for the body of Foo::any() (had the programmer used the derive macro instead).

Limitations

The fields need to have Arbitrary implementations; there is no support for recursive derivation. See the tests for examples; this should be resolvable through further engineering effort.

Towards #3832

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Jun 19, 2025
Carolyn Zech added 4 commits June 19, 2025 21:42
@carolynzech carolynzech force-pushed the autoharness-derive-arbitrary branch from 8d32535 to 8cb3b04 Compare June 20, 2025 01:46
@carolynzech carolynzech marked this pull request as ready for review June 20, 2025 01:47
@carolynzech carolynzech requested a review from a team as a code owner June 20, 2025 01:47
@carolynzech
Copy link
Contributor Author

carolynzech commented Jun 20, 2025

I recommend reviewing commit-by-commit. In the first commit, review in execution order: i.e., first look at the changes in codegen_units.rs, then kani_middle::mod.rs, then automatic.rs.

@github-actions github-actions bot added the Z-CompilerBenchCI Tag a PR to run benchmark CI label Jun 24, 2025
@tautschnig tautschnig added this pull request to the merge queue Jun 27, 2025
Merged via the queue into model-checking:main with commit 0024103 Jun 27, 2025
27 of 28 checks passed
@carolynzech carolynzech deleted the autoharness-derive-arbitrary branch June 27, 2025 14:46
@carolynzech carolynzech mentioned this pull request Jul 2, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jul 3, 2025
Automatic Derivation Fixes (#4194)
5b6519b 
Fixes and improvements to the derivation of Arbitrary in the compiler
introduced in #4167, along with a fix for #4189 and some other small
improvements to autoharness that I noticed along the way. Best reviewed
commit by commit.

Resolves #4189
Towards #3832 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
@carolynzech carolynzech mentioned this pull request Jul 3, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Jul 3, 2025
Bump Kani version to 0.64.0 (#4198)
96f7e59 
Auto generated release notes:

## What's Changed
* Edit quantifiers' documentation. by @thanhnguyen-aws in
#4142
* Fix the bug of using multiple hidden variables for the prev of the
same Expr by @thanhnguyen-aws in
#4150
* Remove `assess` subcommand by @carolynzech in
#4111
* Optimize goto binary exporting in `cprover_bindings` by
@AlexanderPortland in #4148
* Add the option to generate performance flamegraphs by
@AlexanderPortland in #4138
* Fix the bug: Static union values can panic Kani by @thanhnguyen-aws in
#4112
* Update toolchain to 2025-06-13 by @carolynzech in
#4152
* Automatic cargo update to 2025-06-16 by @github-actions in
#4156
* Major-version update cargo dependencies by @tautschnig in
#4158
* Upgrade Rust toolchain to 2025-06-16 by @tautschnig in
#4157
* Bump tests/perf/s2n-quic from `3129ad5` to `c6e694e` by @dependabot in
#4160
* Bump tests/perf/s2n-quic from `c6e694e` to `b1b5bf8` by @dependabot in
#4164
* Upgrade Rust toolchain to 2025-06-17 by @tautschnig in
#4163
* Automatic cargo update to 2025-06-23 by @github-actions in
#4172
* Stub panics during MIR transformation by @AlexanderPortland in
#4169
* Bump tests/perf/s2n-quic from `b1b5bf8` to `32ba87d` by @dependabot in
#4175
* Handle enums with zero or one variants by @zhassan-aws in
#4171
* Introduce compiler timing script & CI job by @AlexanderPortland in
#4154
* Upgrade Rust toolchain to 2025-06-18 by @tautschnig in
#4166
* Cache dependencies for CI jobs by @AlexanderPortland in
#4181
* Autoharness: Derive `Arbitrary` for structs and enums by @carolynzech
in #4167
* Upgrade Rust toolchain to 2025-06-27 by @tautschnig in
#4182
* Include wget in dependencies by @zhassan-aws in
#4183
* Automatic cargo update to 2025-06-30 by @github-actions in
#4186
* Add support for loop assigns in loop contracts by @thanhnguyen-aws in
#4174
* Upgrade toolchain to 06/30 by @carolynzech in
#4188
* Optimize reachability with non-mutating global passes by
@AlexanderPortland in #4177
* Bump tests/perf/s2n-quic from `32ba87d` to `b8f8cca` by @dependabot in
#4190
* Bump ncipollo/release-action from 1.16.0 to 1.18.0 by @dependabot in
#4191
* Upgrade toolchain to 07/02 by @carolynzech in
#4195
* Automatic Derivation Fixes by @carolynzech in
#4194


**Full Changelog**:
kani-0.63.0...kani-0.64.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnig tautschnig tautschnig approved these changes

Assignees

No one assigned

Labels

Z-CompilerBenchCI Tag a PR to run benchmark CI Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@carolynzech @tautschnig